////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2008, 2009 The Mist project                                  //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the echo wrapper.
///

#include "echo.hpp"

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <boost/foreach.hpp>
#define foreach BOOST_FOREACH

#include <boost/algorithm/string/replace.hpp>
using boost::replace_all;

#include <boost/assign.hpp>
using namespace boost::assign;

#include "common/assert.hpp"
#include "common/ptr.hpp"
#include "common/string.hpp"
#include "codestream.hpp"
#include "copyast.hpp"
#include "nodes.hpp"
#include "operator.hpp"
#include "parse.hpp"
#include "tree.hpp"
#include "visitor.hpp"

////////////////////////////////////////////////////////////////////////////////
// EchoVisitor Class                                                          //
////////////////////////////////////////////////////////////////////////////////

/// Visits the nodes of an abstract syntax tree to echo the program to a
/// stream. A visitor in the visitor pattern.
///
class EchoVisitor : public Visitor {
	public:
		
		/// Construct an echo visitor.
		///
		EchoVisitor(
			ostream& out,    ///< the stream to send the echo to
			uint     info,   ///< what additional information to output
			uint     tabSize ///< the tab-size to use in the output
		);
		
		~EchoVisitor();
		
		VISIT_FUNCTIONS_FROM( CONCRETE_NODES )
	
	private:
		
		void visit_statement(wptr<Statement> node);
		
		void visit_compoundstatement(wptr<CompoundStatement> node);
		
		void print_proof(wptr<KeySolver> solver, string description);
		
		CodeStream& cdout;
		
		uint _info;
		
		uint _implicationNr;
};

/// \return true , if the \a inner operation should have parentheses
///         false, otherwise
///
bool needs_parentheses(
	wptr<Operator> outer, ///< the outer operation
	wptr<Operator> inner, ///< the inner operation
	bool firstOperand,    ///< whether \a inner is the first operand of \a outer
	bool lastOperand      ///< whether \a inner is the last  operand of \a outer
);

////////////////////////////////////////////////////////////////////////////////
// Function Implementations                                                   //
////////////////////////////////////////////////////////////////////////////////

echo::echo(wptr<Node> tree, uint info, uint tabSize) : _tree(tree), _info(info), _tabSize(tabSize) {
	assert(tree);
}

ostream& echo::send_to_stream(ostream& out) const {
	sptr<EchoVisitor> visitor(new EchoVisitor(out, _info, _tabSize));
	
	_tree->accept(visitor);
	
	return out;
}

////////////////////////////////////////////////////////////////////////////////

EchoVisitor::EchoVisitor(ostream& out, uint info, uint tabSize) : cdout(*new CodeStream(out, tabSize)), _info(info), _implicationNr(0) {
} // intentionally empty

EchoVisitor::~EchoVisitor() {
	delete &cdout;
}

void EchoVisitor::visit(wptr<Declarations> node) {
	assert(node);
	
	bool newline = false;
	foreach (wptr<Declaration> d, node->declarations) {
		if (d->location->begin.file != "base.m") {
			if (newline++) cdout << "\n";
			d->accept(wptr_this());
		}
	}
}

void EchoVisitor::visit(wptr<AssertionArea> node) {
	assert(node);
	
	foreach (wptr<Expression> e, node->conditions) {
		cdout << "@ ";
		e->accept(wptr_this());
		cdout << ";\n";
	}
	
	if (node->conditions.empty())
		cdout << "@\n";
}

void EchoVisitor::visit(wptr<IfStatement> node) {
	assert(node);
	
	cdout << "if (";
	node->condition->accept(wptr_this());
	cdout << ")";
	
	{
		bool compound = (typeid(*node->thenStatement) == typeid(CompoundStatement));
		
		if (compound) cdout << " ";
		else          cdout << "\n" << indent;
		
		visit_statement(node->thenStatement);
		
		if (!compound) cdout << unindent;
	}
	
	if (node->elseStatement) {
		cdout << "else";
		
		bool compound = (typeid(*node->elseStatement) == typeid(CompoundStatement));
		
		if (compound) cdout << " ";
		else          cdout << "\n" << indent;
		
		visit_statement(node->elseStatement);
		
		if (!compound) cdout << unindent;
	}
}

void EchoVisitor::visit(wptr<WhileStatement> node) {
	assert(node);
	
	cdout << "while (";
	node->condition->accept(wptr_this());
	cdout << ")";
	
	bool simple = node->statement.size() == 1
	           && node->invariant.size() == 0
	           && node->bound    .size() == 0;
	
	if (!simple)
		cdout << "\n";
	
	foreach (wptr<Expression> bound, node->bound) {
		cdout << "bound (";
		bound->accept(wptr_this());
		cdout << ")\n";
	}
	
	foreach (wptr<AssertionArea> invariant, node->invariant) {
		cdout << "invariant";
		
		cdout << " {" << "\n" << indent;
			
		visit_statement(invariant);
		
		cdout << unindent << "}\n";
	}
	
	foreach (wptr<Statement> statement, node->statement) {
		bool compound = (typeid(*statement) == typeid(CompoundStatement));
		
		if (!simple) cdout << "do";
		
		if (compound) cdout << " ";
		else          cdout << "\n" << indent;
		
		visit_statement(statement);
		
		if (!compound) cdout << unindent;
	}
	
	cdout << "\n";
	
	if ((_info & echo::TotalCorrectnessOutline) && node->totalPostImplicationSolver)
		print_proof(node->totalPostImplicationSolver, "total correctness");
	
	if ((_info & echo::PartialCorrectnessOutline) && node->partialPostImplicationSolver)
		print_proof(node->partialPostImplicationSolver, "partial correctness");
}

void EchoVisitor::visit(wptr<ForStatement> node) {
	assert(node);
	
	cdout << "for (";
	node->iteratorType->accept(wptr_this());
	cdout << " ";
	node->iterator->accept(wptr_this());
	cdout << ", ";
	node->collection->accept(wptr_this());
	cdout << ")";
	
	bool simple = node->statement.size() == 1
	           && node->invariant.size() == 0;
	
	if (!simple)
		cdout << "\n";
	
	foreach (wptr<AssertionArea> invariant, node->invariant) {
		bool compound = (typeid(*invariant) == typeid(CompoundStatement));
		
		cdout << "invariant";
		
		if (compound) cdout << " ";
		else          cdout << "\n" << indent;
			
		visit_statement(invariant);
		
		if (!compound) cdout << unindent;
	}
	
	foreach (wptr<Statement> statement, node->statement) {
		bool compound = (typeid(*statement) == typeid(CompoundStatement));
		
		if (!simple) cdout << "do";
		
		if (compound) cdout << " ";
		else          cdout << "\n" << indent;
		
		visit_statement(statement);
		
		if (!compound) cdout << unindent;
	}
}

void EchoVisitor::visit(wptr<CompoundStatement> node) {
	assert(node);
	
	visit_compoundstatement(node);
}

void EchoVisitor::visit(wptr<CppStatement> node) {
	assert(node);
	
	cdout << "cpp \"" << escape_string(node->code) << "\";\n";
}

void EchoVisitor::visit(wptr<VariableDeclaration> node) {
	assert(node);
	
	node->type->accept(wptr_this());
	cdout << " ";
	
	bool comma = false;
	foreach (VariableDeclaration::Pair var, node->pairs) {
		if (comma++) cdout << ", ";
		var.name->accept(wptr_this());
		if (var.init) {
			cdout << " <- ";
			var.init->accept(wptr_this());
		}
	}
	
	cdout << ";\n";
}

void EchoVisitor::visit(wptr<TypeDeclaration> node) {
	assert(node);
	
	cdout << "type ";
	node->name->accept(wptr_this());
	cdout << " cpp \"" << escape_string(node->cpp) << "\"";
	cdout << " KeY \"" << escape_string(node->KeY) << "\";\n";
}

void EchoVisitor::visit(wptr<TypeType> node) {
	assert(node);
	
	cdout << "type";
}

void EchoVisitor::visit(wptr<FunctionDeclaration> node) {
	assert(node);
	
	if (!node->isTemplateInstantiation) {
		// Return type
		//
		node->type->returnType->accept(wptr_this());
		
		cdout << " ";
		
		// Function name
		//
		node->name->accept(wptr_this());
		
		// Template type declaration
		//
		if (node->templateTypeNames.size() > 0) {
			cdout << "?(";
			bool comma = false;
			foreach(wptr<Identifier> name, node->templateTypeNames) {
				if (comma++) cdout << ", ";
				name->accept(wptr_this());
			}
			cdout << ")";
		}
		
		// Function parameters
		//
		cdout << "(";
		bool comma = false;
		foreach (FunctionDeclaration::Parameter p, node->parameters()) {
			if (comma++) cdout << ", ";
			p.type->accept(wptr_this());
			cdout << " ";
			p.name->accept(wptr_this());
		}
		cdout << ")";
		
		if (node->ensurance)
			cdout << " ensure";
		
		bool simple = node->body       .size() == 1
		           && node->logicalVars.size() == 0
		           && node->pre        .size() == 0
		           && node->post       .size() == 0
		           && node->KeY        .size() == 0
		           && node->bound      .size() == 0
		           && !(_info & echo::PartialCorrectnessOutline);
		
		if (!simple)
			cdout << "\n";
		
		foreach (wptr<Expression> bound, node->bound) {
			cdout << "bound (";
			bound->accept(wptr_this());
			cdout << ")\n";
		}
		
		foreach (wptr<VariableDeclaration> vardec, node->logicalVars) {
			cdout << "logical ";
			visit_statement(vardec);
		}
		
		foreach (wptr<AssertionArea> pre, node->pre) {
			cdout << "pre {\n" << indent;
			visit_statement(pre);
			cdout << unindent << "}\n";
		}
		
		if ((_info & echo::PartialCorrectnessOutline) && node->pre.size() == 0 && node->KeY.size() == 0) {
			cdout << "pre {\n" << indent << "@ true;" << unindent << "\n}\n";
		}
		
		foreach (wptr<CompoundStatement> body, node->body) {
			if (!simple) cdout << "body ";
			visit_statement(body);
		}
		
		foreach (wptr<AssertionArea> post, node->post) {
			cdout << "post {\n" << indent;
			visit_statement(post);
			cdout << unindent << "}\n";
		}
		
		if ((_info & echo::PartialCorrectnessOutline) && node->post.size() == 0 && node->KeY.size() == 0) {
			cdout << "post {\n" << indent << "@ true;" << unindent << "\n}\n";
		}
		
		foreach (string KeY, node->KeY) {
			cdout << "KeY \"" << escape_string(KeY) << "\"\n";
		}
	}
}

void EchoVisitor::visit(wptr<FunctionCall> node) {
	assert(node);
	
	node->base->accept(wptr_this());
	cdout << "(";
	bool comma = false;
	foreach (wptr<Expression> param, node->parameters) {
		if (comma++) cdout << ", ";
		param->accept(wptr_this());
	}
	cdout << ")";
}

void EchoVisitor::visit(wptr<OperatorCall> node) {
	assert(node);
	
	uint operand = 0;
	for (uint i = 0; i < node->op->echo().size(); ++i) {
		bool first = (i == 0);
		bool last  = (i == node->op->echo().size() - 1);
		if (node->op->echo()[i].empty()) {
			wptr<Operator> outer = node->op;
			wptr<Operator> inner;
			if (typeid(*node->operands[operand]) == typeid(OperatorCall))
				inner = node->operands[operand].cast<OperatorCall>()->op;
			else if (typeid(*node->operands[operand]) == typeid(ChainExpression))
				inner = node->operands[operand].cast<ChainExpression>()->operators[0];
			if (!(*node->op == SingleOperator("1 [ 2 ]") && i > 0) // Inside array brackets, no parentheses needed
			    && inner                                           // Without an inner operand, no parentheses needed
			    && needs_parentheses(outer, inner, first, last)) { // Otherwise, check precedence and associativity
				cdout << "(";
				node->operands[operand]->accept(wptr_this());
				cdout << ")";
			} else {
				node->operands[operand]->accept(wptr_this());
			}
			++operand;
		} else {
			cdout << node->op->echo()[i];
		}
		if (!last)
			cdout << string(node->op->spaces(), ' ');
	}
}

void EchoVisitor::visit(wptr<Reference> node) {
	assert(node);
	
	if (node->scopePart) {
		node->scopePart->accept(wptr_this());
		cdout << ".";
	}
	
	if (node->namePart)
		cdout << *node->namePart;
	
	if (node->formalTypeSpec) {
		cdout << "!(";
		bool comma = false;
		foreach (wptr<Type> type, *node->formalTypeSpec) {
			if (comma++) cdout << ", ";
			type->accept(wptr_this());
		}
		cdout << ")";
	}
	
	if (node->templateTypeSpec) {
		cdout << "?(";
		bool comma = false;
		foreach (wptr<Type> type, *node->templateTypeSpec) {
			if (comma++) cdout << ", ";
			type->accept(wptr_this());
		}
		cdout << ")";
	}
}

void EchoVisitor::visit(wptr<BooleanLiteral> node) {
	assert(node);
	
	cdout << (node->value ? "true" : "false");
}

void EchoVisitor::visit(wptr<IntegerLiteral> node) {
	assert(node);
	
	cdout << node->value;
}

void EchoVisitor::visit(wptr<ChainExpression> node) {
	assert(node);
	
	uint operand = 0;
	for (uint j = 0; j < node->operators.size(); ++j) {
		for (uint i = 0; i < node->operators[j]->echo().size() - (j != node->operators.size() - 1); ++i) {
			bool first = (j == 0 && i == 0);
			bool last  = (j == node->operators.size() - 1 && i == node->operators[j]->echo().size() - 1);
			if (node->operators[j]->echo()[i].empty()) {
				wptr<Operator> outer = node->operators[j];
				wptr<Operator> inner;
				if (typeid(*node->operands[operand]) == typeid(OperatorCall))
					inner = node->operands[operand].cast<OperatorCall>()->op;
				else if (typeid(*node->operands[operand]) == typeid(ChainExpression))
					inner = node->operands[operand].cast<ChainExpression>()->operators[0];
				
				if (inner && needs_parentheses(outer, inner, first, last)) {
					cdout << "(";
					node->operands[operand]->accept(wptr_this());
					cdout << ")";
				} else {
					node->operands[operand]->accept(wptr_this());
				}
				++operand;
			} else {
				cdout << node->operators[j]->echo()[i];
			}
			
			if (!last)
				cdout << string(node->operators[j]->spaces(), ' ');
		}
	}
}

void EchoVisitor::visit(wptr<FunctionType> node) {
	assert(node);
	
	node->returnType->accept(wptr_this());
	cdout << "(";
	for (uint i = 0; i < node->parameterTypes.size(); ++i) {
		node->parameterTypes[i]->accept(wptr_this());
		if (i < node->parameterTypes.size() - 1)
			cdout << ", ";
	}
	cdout << ")";
}

void EchoVisitor::visit(wptr<PointerType> node) {
	assert(node);
	
	node->type->accept(wptr_this());
	switch (node->strength) {
		case PointerType::STRONG_POINTER:  cdout << "^"; break;
		case PointerType::WEAK_POINTER:    cdout << "`"; break;
		default: assert(false);
	}
}

void EchoVisitor::visit(wptr<ArrayType> node) {
	assert(node);
	
	node->type->accept(wptr_this());
	cdout << "[]";
}

void EchoVisitor::visit(wptr<NamedType> node) {
	assert(node);
	
	node->reference->accept(wptr_this());
}

void EchoVisitor::visit(wptr<VoidType> node) {
	assert(node);
	
	cdout << "void";
}

void EchoVisitor::visit(wptr<Identifier> node) {
	assert(node);
	
	cdout << node->text;
}

void EchoVisitor::visit_statement(wptr<Statement> node) {
	assert(node);
	
	node->accept(wptr_this());
	if (   typeid(*node) == typeid(OperatorCall)
	    || typeid(*node) == typeid(FunctionCall))
	    cdout << ";\n";
}

void EchoVisitor::visit_compoundstatement(wptr<CompoundStatement> node) {
	assert(node);
	
	if (node->name) {
		node->name->accept(wptr_this());
		cdout << " ";
	}
	
	if (node->statements.size() == 0) {
		cdout << "{";
		
		if (typeid(*node->parent) == typeid(FunctionDeclaration) && _info) {
			cdout << "\n" << indent;
			
			if ((_info & echo::TotalCorrectnessOutline) && node->parent.cast<FunctionDeclaration>()->totalPreImplicationSolver)
				print_proof(node->parent.cast<FunctionDeclaration>()->totalPreImplicationSolver, "total correctness");
			
			if ((_info & echo::PartialCorrectnessOutline) && node->parent.cast<FunctionDeclaration>()->partialPreImplicationSolver)
				print_proof(node->parent.cast<FunctionDeclaration>()->partialPreImplicationSolver, "partial correctness");
			
			cdout << "\n" << unindent;
		} else if (typeid(*node->parent) == typeid(WhileStatement) && _info) {
			cdout << "\n" << indent;
			
			if ((_info & echo::TotalCorrectnessOutline) && node->parent.cast<WhileStatement>()->totalPreImplicationSolver)
				print_proof(node->parent.cast<WhileStatement>()->totalPreImplicationSolver, "total correctness");
			
			if ((_info & echo::PartialCorrectnessOutline) && node->parent.cast<WhileStatement>()->partialPreImplicationSolver)
				print_proof(node->parent.cast<WhileStatement>()->partialPreImplicationSolver, "partial correctness");
			
			cdout << "\n" << unindent;
		}
		
		cdout << "}\n";
	} else {
		cdout << "{\n" << indent;
		
		if (typeid(*node->parent) == typeid(FunctionDeclaration)) {
			if ((_info & echo::TotalCorrectnessOutline) && node->parent.cast<FunctionDeclaration>()->totalPreImplicationSolver)
				print_proof(node->parent.cast<FunctionDeclaration>()->totalPreImplicationSolver, "total correctness");
			
			if ((_info & echo::PartialCorrectnessOutline) && node->parent.cast<FunctionDeclaration>()->partialPreImplicationSolver)
				print_proof(node->parent.cast<FunctionDeclaration>()->partialPreImplicationSolver, "partial correctness");
			
			cdout << "\n";
		} else if (typeid(*node->parent) == typeid(WhileStatement)) {
			if ((_info & echo::TotalCorrectnessOutline) && node->parent.cast<WhileStatement>()->totalPreImplicationSolver)
				print_proof(node->parent.cast<WhileStatement>()->totalPreImplicationSolver, "total correctness");
			
			if ((_info & echo::PartialCorrectnessOutline) && node->parent.cast<WhileStatement>()->partialPreImplicationSolver)
				print_proof(node->parent.cast<WhileStatement>()->partialPreImplicationSolver, "partial correctness");
			
			cdout << "\n";
		}
		
		foreach (wptr<Statement> statement, node->statements) {
			if (_info & echo::TotalCorrectnessOutline && statement->totalPrecondition) {
				cdout << "| proof outline (total correctness)\n"
				      << "@ ";
				statement->totalPrecondition->accept(wptr_this());
				cdout << ";\n";
			}
			if (_info & echo::PartialCorrectnessOutline && statement->partialPrecondition) {
				cdout << "| proof outline (partial correctness)\n"
				      << "@ ";
				statement->partialPrecondition->accept(wptr_this());
				cdout << ";\n";
			}
			if (_info)
				cdout << "\n";
			
			visit_statement(statement);
			
			if (_info)
				cdout << "\n";
		}
		
		if (_info & echo::TotalCorrectnessOutline && node->totalPostcondition) {
			cdout << "| proof outline (total correctness)\n"
				  << "@ ";
			node->totalPostcondition->accept(wptr_this());
			cdout << ";\n";
		}
		if (_info & echo::PartialCorrectnessOutline && node->partialPostcondition) {
			cdout << "| proof outline (partial correctness)\n"
				  << "@ ";
			node->partialPostcondition->accept(wptr_this());
			cdout << ";\n";
		}
		
		cdout << unindent << "}\n";
	}
}

void EchoVisitor::print_proof(wptr<KeySolver> solver, string description) {
	if (solver->proof_status() == KeySolver::FAILED)
		cdout << "| PROOF FAILED (" + description + ")\n| @ ";
	else if (solver->proof_status() == KeySolver::TIMEOUT)
		cdout << "| PROOF TIMEOUT (" + description + "): " << solver->proof_file() << "\n@ ";
	else if (solver->proof_status() == KeySolver::NOT_PROVED)
		cdout << "| NO PROOF FOUND (" + description + "): " << solver->proof_file() << "\n@ ";
	else if (solver->proof_status() == KeySolver::PROVED)
		cdout << "| PROVED (" + description + "): " << solver->proof_file() << "\n@ ";
	solver->problem()->accept(wptr_this());
	cdout << ";\n";
}

////////////////////////////////////////////////////////////////////////////////

bool needs_parentheses(wptr<Operator> outer, wptr<Operator> inner, bool firstOperand, bool lastOperand) {
	assert(outer);
	assert(inner);
	
	// If the outer operator binds tighter than the inner operator.
	//
	if (outer->binds_tighter_than(inner))
		return true;
	
	// If the inner operator binds tighter than the outer operator.
	//
	if (inner->binds_tighter_than(outer))
		return false;
	
	// If the inner and outer operators have the same precedence.
	//
	if (  (firstOperand && outer->associativity() == RIGHT_ASSOCIATIVE)
	    || (lastOperand && outer->associativity() ==  LEFT_ASSOCIATIVE)
	    ||                (outer->associativity() == CHAIN_ASSOCIATIVE)
	    ||                (outer->associativity() ==   NON_ASSOCIATIVE))
		return true;
	
	return false;
}
